p  q == if p then q else ff fi  

latex

Up	bool 1, bool 1
Wellformedness Lemmas	band wf, band wf
Definitions	if b then t else f fi , ff